DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2011.233

System T and the Product of Selection Functions

Authors: Martin Escardo, Paulo Oliva, and Thomas Powell

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract

We show that the finite product of selection functions (for all finite types) is primitive recursively equivalent to Goedel's higher-type recursor (for all finite types). The correspondence is shown to hold for similar restricted fragments of both systems: The recursor for type level n+1 is primitive recursively equivalent to the finite product of selection functions of type level n. Whereas the recursor directly interprets induction, we show that other classical arithmetical principles such as bounded collection and finite choice are more naturally interpreted via the product of selection functions.

Cite as

Martin Escardo, Paulo Oliva, and Thomas Powell. System T and the Product of Selection Functions. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 233-247, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{escardo_et_al:LIPIcs.CSL.2011.233,
  author =	{Escardo, Martin and Oliva, Paulo and Powell, Thomas},
  title =	{{System T and the Product of Selection Functions}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{233--247},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.233},
  URN =		{urn:nbn:de:0030-drops-32341},
  doi =		{10.4230/LIPIcs.CSL.2011.233},
  annote =	{Keywords: primitive recursion, product of selection functions, finite choice, dialectica interpretation}
}

Search Results

Documents authored by Powell, Thomas

System T and the Product of Selection Functions

Abstract

Cite as

Thanks for your feedback!

Could not send message